﻿//using System;
//using System.Collections.Generic;
//using System.Text;
//using Microsoft.Cci;
//using Microsoft.Cci.MutableCodeModel;

//namespace Tool
//{
//    class DummyPathAdder : CodeMutator
//    {
//        private CodeMutator normalMutator;
//        private Microsoft.Cci.MutableCodeModel.MethodReference methodReference;

//        public DummyPathAdder(HostEnvironment host, SourceMethodBodyProvider ilToSourceProvider, SourceToILConverterProvider sourceToILProvider, ISourceLocationProvider/*?*/ sourceLocationProvider)
//            : base(host, ilToSourceProvider, sourceToILProvider, sourceLocationProvider)
//        {
//            normalMutator = new CodeMutator(host, ilToSourceProvider, sourceToILProvider, sourceLocationProvider);
//        }

//        public override IExpression Visit(MethodCall methodCall)
//        {
//            if (methodCall.MethodToCall.Name.Value == "IsTrue")
//            {
//                if (methodReference == null)
//                {
//                    this.methodReference = methodCall.MethodToCall as Microsoft.Cci.MutableCodeModel.MethodReference;
                    

//                }
//            }
//            return base.Visit(methodCall);
//        }
        
//        public override IBlockStatement Visit(BlockStatement blockStatement)
//        {
//            List<IStatement> statements = blockStatement.Statements;
//            List<IStatement> newList = new List<IStatement>();
//            foreach (var statement in statements)
//            {
//                IExpressionStatement expression = statement as IExpressionStatement;
//                if (expression != null)
//                {
//                    IAssignment assign = expression.Expression as IAssignment;
//                    if (assign != null)
//                    {
//                        Statement constraint = ExtractCondition(assign);
//                        if (constraint != CodeDummy.Block)
//                        {
//                            if (constraint as BlockStatement != null)
//                            {
//                                newList.AddRange((constraint as BlockStatement).Statements);
//                            }
//                            else
//                            {
//                                newList.Add(constraint);
//                            }
//                        }
//                    }
//                }
//                IConditionalStatement conditional = statement as IConditionalStatement;
//                if (conditional != null)
//                {
//                    Statement constraint = getConstraints(conditional);
//                    if (constraint != CodeDummy.Block)
//                    {
//                        if (constraint as BlockStatement != null)
//                        {
//                            newList.AddRange((constraint as BlockStatement).Statements);
//                        }
//                        else
//                        {
//                            newList.Add(constraint);
//                        }
//                    }
//                }

                
//                newList.Add(statement);
//            }
//            blockStatement.Statements = newList;
//            blockStatement.Statements = Visit(blockStatement.Statements);
//            return blockStatement;
//        }

//        private Statement getConstraints(IConditionalStatement conditionalStatement)
//        {
//            Statement statement = ExtractCondition(conditionalStatement.Condition as IExpression);
//            return statement;
//        }

//        private Statement ExtractCondition(IExpression expression)
//        {
//            if (expression as GreaterThan != null)
//            {
//                IStatement stmt = Traverse(expression as GreaterThan);
//                return stmt as Statement;
//            }
//            else if (expression as LessThan != null)
//            {
//                IStatement stmt = Traverse(expression as LessThan);
//                return stmt as Statement;
//            }
//            else if (expression as LogicalNot != null)
//            {
//                IStatement stmt = Traverse(expression as LogicalNot);
//                return stmt as Statement;
                
//            }
//            else if (expression as Conditional != null)
//            {
//                List<IExpression> clauseList = ExtractClauses(expression as Conditional);
//                List<IExpression> clauseList2 = new List<IExpression>();
//                clauseList2.AddRange(clauseList);

//                IStatement stmt = Traverse(clauseList);
//                List<IStatement> stmtList = (stmt as BlockStatement).Statements;
//                foreach (IExpression exp in clauseList2)
//                {
//                    BlockStatement blkstmt = ExtractCondition(exp) as BlockStatement;
//                    if(blkstmt != null)
//                        stmtList.AddRange(blkstmt.Statements);
//                }
                
                
                
//                return stmt as Statement;
//            }
//            else if (expression as Equality != null)
//            {
//                IStatement stmt = Traverse(expression as Equality);
//                return stmt as Statement;
//            }
//            else if (expression as LessThanOrEqual != null)
//            {
//                GreaterThan gt = new GreaterThan();
//                gt.LeftOperand = (expression as LessThanOrEqual).LeftOperand;
//                gt.RightOperand = (expression as LessThanOrEqual).RightOperand;
//                IStatement stmt = Traverse(gt);
//                return stmt as Statement;
                
//            }
//            else if (expression as GreaterThanOrEqual != null)
//            {
//                LessThan lt = new LessThan();
//                lt.LeftOperand = (expression as GreaterThanOrEqual).LeftOperand;
//                lt.RightOperand = (expression as GreaterThanOrEqual).RightOperand;
//                IStatement stmt = Traverse(lt);
//                return stmt as Statement;
//            }
//            return new AssumeStatement() as Statement;
//        }

//        private IStatement Traverse(List<IExpression> clauseList)
//        {
//            BlockStatement block = new BlockStatement();
//            List<IStatement> stmntList = new List<IStatement>();

//            LocalDeclarationStatement localDeclare = new LocalDeclarationStatement();
            
//            LocalDefinition localDef = new LocalDefinition();
//            localDef.Name = this.host.NameTable.GetNameFor("aaaaaaaaaaaa");
//            localDef.Type = this.host.PlatformType.SystemBoolean;
//            localDeclare.LocalVariable = localDef;
            
//            CompileTimeConstant initialValue = new CompileTimeConstant();
//            initialValue.Value = true;
//            initialValue.Type = this.host.PlatformType.SystemBoolean;
            
//            localDeclare.InitialValue = initialValue;
            
//            List<IStatement> tempBuffer = new List<IStatement>();
//            tempBuffer.Add(localDeclare);

//            BoundExpression tempvar = new BoundExpression();
//            tempvar.Type = this.host.PlatformType.SystemBoolean;
//            tempvar.Definition = localDef;

//            TargetExpression holder = new TargetExpression();
//            holder.Type = this.host.PlatformType.SystemBoolean;
//            holder.Definition = localDef;
            
//            BuildConditions(clauseList, stmntList, tempBuffer, tempvar, holder);
//            block.Statements = stmntList;
//            return block as IStatement;
//        }

//        private void BuildConditions(List<IExpression> clauseList, List<IStatement> stmntList, 
//            List<IStatement> tempBuffer, BoundExpression tempvar, TargetExpression holder)
//        {
//            IExpression predicate = clauseList[0];
//            clauseList.Remove(predicate);
//            List<IExpression> clauseList1 = new List<IExpression>();
//            clauseList1.AddRange(clauseList);

//            CompileTimeConstant cons = new CompileTimeConstant();
//            cons.Value = false;
//            cons.Type = this.host.PlatformType.SystemBoolean;

//            CompileTimeConstant cons1 = new CompileTimeConstant();
//            cons1.Value = true;
//            cons1.Type = this.host.PlatformType.SystemBoolean;

//            Equality eq = new Equality();
//            eq.LeftOperand = predicate;
//            eq.RightOperand = cons1;
            
//            Conditional conditionalTrue = new Conditional();
//            conditionalTrue.Condition = tempvar as IExpression;
//            conditionalTrue.ResultIfFalse = cons;
//            conditionalTrue.ResultIfTrue = eq;

//            ExpressionStatement statement = new ExpressionStatement();
//            Assignment assignment = new Assignment();
//            assignment.Target = holder;
//            assignment.Source = conditionalTrue as IExpression;
//            statement.Expression = assignment as IExpression;
//            tempBuffer.Add(statement);

//            if (clauseList1.Count != 0)
//            {
//                BuildConditions(clauseList1, stmntList, tempBuffer, tempvar, holder);
//            }
//            else
//            {
//                stmntList.AddRange(tempBuffer);
//                stmntList.Add(GetConstraint(tempvar as IExpression));
//            }
//            tempBuffer.Remove(statement);
//            clauseList1.RemoveRange(0,clauseList1.Count);
//            clauseList1.AddRange(clauseList);
//            Equality eq2 = new Equality();
//            eq2.LeftOperand = predicate;
//            eq2.RightOperand = cons;
            
//            Conditional conditionalFalse = new Conditional();
//            conditionalFalse.Condition = tempvar as IExpression;
//            conditionalFalse.ResultIfFalse = cons;
//            conditionalFalse.ResultIfTrue = eq2;

//            ExpressionStatement statement2 = new ExpressionStatement();
//            Assignment assignment2 = new Assignment();
//            assignment2.Target = holder;
//            assignment2.Source = conditionalFalse as IExpression;
//            statement2.Expression = assignment2 as IExpression;
//            tempBuffer.Add(statement2);

//            if (clauseList1.Count != 0)
//            {
//                BuildConditions(clauseList1, stmntList, tempBuffer, tempvar, holder);
//            }
//            else
//            {
//                stmntList.AddRange(tempBuffer);
//                stmntList.Add(GetConstraint(tempvar as IExpression));
//            }
//            tempBuffer.Remove(statement2);
//        }

//        private IStatement Traverse(Equality equality)
//        {
//            BlockStatement block = new BlockStatement();
//            List<IStatement> stmntList = new List<IStatement>();

//            if (equality.LeftOperand as IExpression != null)
//            {
//                IStatement stmnt = ExtractCondition(equality.LeftOperand) as IStatement;
//                if (stmnt as BlockStatement != null)
//                    return stmnt;
//            }
            
//            Boolean isnumerical = false;
//            if (equality.RightOperand.Type.ToString() == ("System.Int32"))
//                isnumerical = true;

//            if (isnumerical)
//            {
//                CompileTimeConstant cons = new CompileTimeConstant();
//                cons.Value = 1;

//                Addition add = new Addition();
//                add.LeftOperand = equality.RightOperand;
//                add.RightOperand = cons;

//                Subtraction sub = new Subtraction();
//                sub.LeftOperand = equality.RightOperand;
//                sub.RightOperand = cons;

//                Equality eq = new Equality();
//                eq.LeftOperand = equality.LeftOperand;
//                eq.RightOperand = add;
//                stmntList.Add(GetConstraint(eq as IExpression));

//                Equality eq2 = new Equality();
//                eq2.LeftOperand = equality.LeftOperand;
//                eq2.RightOperand = sub;
//                stmntList.Add(GetConstraint(eq2 as IExpression));

//                Equality eq3 = new Equality();
//                eq3.LeftOperand = equality.LeftOperand;
//                eq3.RightOperand = equality.RightOperand;
//                stmntList.Add(GetConstraint(eq3 as IExpression));

//                block.Statements = stmntList;
                

//            }
//            return block as IStatement;
//        }

//        private IStatement Traverse(LogicalNot logicalNot)
//        {
//            Statement stmt = ExtractCondition(logicalNot.Operand as Expression);
//            return stmt as IStatement;
//        }

//        private List<IExpression> ExtractClauses(Conditional conditional)
//        {
//            List<IExpression> clauseList = new List<IExpression>();
//            IExpression condition = conditional.Condition;
//            if (condition as LogicalNot != null)
//            {
//                condition = (condition as LogicalNot).Operand;
//            }

//            if (condition as Conditional != null)
//            {
//                clauseList.AddRange(ExtractClauses(condition as Conditional));
//            }
//            else
//            {
//                clauseList.Add(condition);
//            }
//            IExpression resultIfTrue = conditional.ResultIfTrue;
//            if (resultIfTrue as LogicalNot != null)
//            {
//                resultIfTrue = (resultIfTrue as LogicalNot).Operand;
//            }
            
//            IExpression resultIfFalse = conditional.ResultIfFalse;
//            if (resultIfFalse as LogicalNot != null)
//            {
//                resultIfFalse = (resultIfFalse as LogicalNot).Operand;
//            }

//            if (resultIfTrue as CompileTimeConstant == null)
//            {
//                if (resultIfTrue as Conditional != null)
//                {
//                    clauseList.AddRange(ExtractClauses(resultIfTrue as Conditional));
//                }
//                else
//                {
//                    clauseList.Add(resultIfTrue);
//                }
//            }
//            if (resultIfFalse as CompileTimeConstant == null)
//            {
//                if (resultIfFalse as Conditional != null)
//                {
//                    clauseList.AddRange(ExtractClauses(resultIfFalse as Conditional));
//                }
//                else
//                {
//                    clauseList.Add(resultIfFalse);
//                }
//            }
//            return clauseList;
//        }
        
//        /*
//         * Exctacting Conditons from "a > b" expression, i.e.,
//         * (a == b+1)||(a > b+1)||(a == b)||(a < b)
//         */
//        private IStatement Traverse(GreaterThan greaterThan)
//        {
//            BlockStatement block = new BlockStatement();
//            List<IStatement> stmntList = new List<IStatement>();

//            CompileTimeConstant cons = new CompileTimeConstant();
//            cons.Value = 1;
            

//            CompileTimeConstant cons1 = new CompileTimeConstant();
//            cons1.Value = true;
//            cons1.Type = this.host.PlatformType.SystemBoolean;
            
//            Addition add = new Addition();
//            add.LeftOperand = greaterThan.RightOperand;
//            add.RightOperand = cons;
            
//            // a == b+1
//            Equality eq = new Equality();
//            eq.LeftOperand = greaterThan.LeftOperand;
//            eq.RightOperand = add;

//            stmntList.Add(GetConstraint(eq as IExpression));

//            // a == b
//            Equality eq2 = new Equality();
//            eq2.LeftOperand = greaterThan.LeftOperand;
//            eq2.RightOperand = greaterThan.RightOperand;

//            stmntList.Add(GetConstraint(eq2 as IExpression));


//            // a > b+1
//            GreaterThan gt = new GreaterThan();
//            gt.LeftOperand = greaterThan.LeftOperand;
//            gt.RightOperand = add;

//            stmntList.Add(GetConstraint(gt as IExpression));


//            // a < b
//            LessThan lt = new LessThan();
//            lt.LeftOperand = greaterThan.LeftOperand;
//            lt.RightOperand = greaterThan.RightOperand;

//            stmntList.Add(GetConstraint(lt as IExpression));


//            block.Statements = stmntList;
//            return block as IStatement; 
//        }

//        private IStatement GetConstraint(IExpression expression)
//        {
//            ConditionalStatement cndstmt = new ConditionalStatement();
//            cndstmt.Condition = expression;
//            cndstmt.TrueBranch = new EmptyStatement();
//            cndstmt.FalseBranch = new EmptyStatement();
//            return cndstmt as IStatement;
//        }

//        /*
//         * Exctacting Conditons from "a < b" expression, i.e.,
//         * (a == b-1)||(a < b-1)||(a == b)||(a > b)
//         */
//        private IStatement Traverse(LessThan lessThan)
//        {
//            BlockStatement block = new BlockStatement();
//            List<IStatement> stmntList = new List<IStatement>();

//            CompileTimeConstant cons = new CompileTimeConstant();
//            cons.Value = 1;

//            Subtraction sub = new Subtraction();
//            sub.LeftOperand = lessThan.RightOperand;
//            sub.RightOperand = cons;
            
//            Equality eq = new Equality();
//            eq.LeftOperand = lessThan.LeftOperand;
//            eq.RightOperand = sub;
//            stmntList.Add(GetConstraint(eq as IExpression));

//            // a < b-1
//            LessThan lt = new LessThan();
//            lt.LeftOperand = lessThan.LeftOperand;
//            lt.RightOperand = sub;
//            stmntList.Add(GetConstraint(lt as IExpression));

//            // a == b
//            Equality eq2 = new Equality();
//            eq2.LeftOperand = lessThan.LeftOperand;
//            eq2.RightOperand = lessThan.RightOperand;
//            stmntList.Add(GetConstraint(eq2 as IExpression));

//            // a > b
//            GreaterThan gt = new GreaterThan();
//            gt.LeftOperand = lessThan.LeftOperand;
//            gt.RightOperand = lessThan.RightOperand;
//            stmntList.Add(GetConstraint(gt as IExpression));

//            block.Statements = stmntList;
//            return block as IStatement; 
//        }
//    }
//}
